\begin{tabbing} R{-}ds($R$;$i$) \\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $R$ of \+ \\[0ex]Rnone =$>$ \\[0ex]Rplus(${\it left}$,${\it right}$)=$>$${\it rec}_{1}$,${\it rec}_{2}$.${\it rec}_{1}$ $\oplus$ ${\it rec}_{2}$ \\[0ex]Rinit(${\it loc}$,$T$,$x$,$v$)=$>$ if ${\it loc}$ = $i$$\rightarrow$ $x$ : $T$ else fi \\[0ex]Rframe(${\it loc}$,$T$,$x$,$L$)=$>$ if ${\it loc}$ = $i$$\rightarrow$ $x$ : $T$ else fi \\[0ex]Rsframe(${\it lnk}$,${\it tag}$,$L$)=$>$ \\[0ex]Reffect(${\it loc}$,${\it ds}$,${\it knd}$,$T$,$x$,$f$)=$>$ if ${\it loc}$ = $i$$\rightarrow$ ${\it ds}$ else fi \\[0ex]Rsends(${\it ds}$,${\it knd}$,$T$,$l$,${\it dt}$,$g$)=$>$ if source($l$) = $i$$\rightarrow$ ${\it ds}$ else fi \\[0ex]Rpre(${\it loc}$,${\it ds}$,$a$,$T$,$P$)=$>$ if ${\it loc}$ = $i$$\rightarrow$ ${\it ds}$ else fi \\[0ex]Raframe(${\it loc}$,$k$,$L$)=$>$ \\[0ex]Rbframe(${\it loc}$,$k$,$L$)=$>$ \\[0ex]Rrframe(${\it loc}$,$x$,$L$)=$>$ \- \end{tabbing}